<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Capabilities | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Capabilities</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="capabilities">Capabilities</h1>

<p>You will learn:</p>
<ol>
  <li>The jargon CNode, CSpace, CSlot.</li>
  <li>How to invoke a capability.</li>
  <li>How to delete and copy CSlots.</li>
</ol>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/hello-world">Hello world</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> capabilities
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>capabilities_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> capabilities
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>capabilities_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="background">Background</h2>

<h3 id="what-is-a-capability">What is a capability?</h3>

<p>A <em>capability</em> is a unique, unforgeable token that gives the possessor
permission to access an entity or object in system. One way to think of a
capability is as a pointer with access rights. There are three kinds of
capabilities in seL4:</p>

<ul>
  <li>capabilities that control access to kernel objects such as thread control blocks,</li>
  <li>capabilities that control access to abstract resources such as <code class="language-plaintext highlighter-rouge">IRQControl</code>, and</li>
  <li>untyped capabilities, that are responsible for memory ranges and allocation
from those (see also the <a href="/Tutorials/untyped.html">Untyped</a> tutorial).</li>
</ul>

<p>In seL4, capabilities to all resources controlled by the kernel are given to the root
task on initialisation. To change the state of any resource, user code can use
the kernel API, available in <code class="language-plaintext highlighter-rouge">libsel4</code> to request an operation on the resource
a specific capability points to.</p>

<p>For example, the root task is provided with a capability to its own thread
control block (TCB), <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code>, a constant defined by <code class="language-plaintext highlighter-rouge">libsel4</code>.
To change the properties of the initial TCB, one can use any of the <a href="https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_tcb">TCB API
methods</a> on this
capability.</p>

<p>Below is an example which changes the stack pointer of the root task’s TCB, a
common operation in the root task if a larger stack is needed:</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_UserContext</span> <span class="n">registers</span><span class="p">;</span>
    <span class="n">seL4_Word</span> <span class="n">num_registers</span> <span class="o">=</span> <span class="k">sizeof</span><span class="p">(</span><span class="n">seL4_UserContext</span><span class="p">)</span><span class="o">/</span><span class="k">sizeof</span><span class="p">(</span><span class="n">seL4_Word</span><span class="p">);</span>

    <span class="cm">/* Read the registers of the TCB that the capability in seL4_CapInitThreadTCB grants access to. */</span>
    <span class="n">seL4_Error</span> <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_ReadRegisters</span><span class="p">(</span><span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">num_registers</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">registers</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="n">seL4_NoError</span><span class="p">);</span>

    <span class="cm">/* set new register values */</span>
    <span class="n">registers</span><span class="p">.</span><span class="n">sp</span> <span class="o">=</span> <span class="n">new_sp</span><span class="p">;</span> <span class="c1">// the new stack pointer, derived by prior code.</span>

    <span class="cm">/* Write new values */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_WriteRegisters</span><span class="p">(</span><span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">num_registers</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">registers</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="n">seL4_NoError</span><span class="p">);</span>
</code></pre></div></div>

<p>The first argument of <code class="language-plaintext highlighter-rouge">seL4_TCB_ReadRegisters</code> and <code class="language-plaintext highlighter-rouge">seL4_TCB_WriteRegisters</code>
addresses the capability in slot <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code>. We will explain
addressing and slots below. The rest of the arguments are specific to the
invocations. Further documentation is available on
<a href="https://docs.sel4.systems/projects/sel4/api-doc.html#read-registers">TCB_ReadRegisters</a>
and
<a href="https://docs.sel4.systems/projects/sel4/api-doc.html#write-registers">TCB_WriteRegisters</a>.</p>

<h3 id="cnodes-and-cslots">CNodes and CSlots</h3>

<p>A <em>CNode</em> (capability-node) is an object full of capabilities: you can think of a CNode as an array of capabilities.
We refer to slots as <em>CSlots</em> (capability-slots). In the example above, <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code> is the slot in the root
task’s CNode that contains the capability to the root task’s TCB.
Each CSlot in a CNode can be in the following state:</p>

<ul>
  <li>empty: the CNode slot contains a null capability,</li>
  <li>full: the slot contains a capability to a kernel resource.</li>
</ul>

<p>By convention the 0th CSlot is kept empty, for the same reasons as keeping NULL unmapped in
 process virtual address spaces: to avoid errors when uninitialised slots are used unintentionally.</p>

<p>The field <code class="language-plaintext highlighter-rouge">info-&gt;CNodeSizeBits</code> gives a measure of the size of the initial
CNode: it will have <code class="language-plaintext highlighter-rouge">1 &lt;&lt; CNodeSizeBits</code> CSlots. A CSlot has
<code class="language-plaintext highlighter-rouge">1 &lt;&lt; seL4_SlotBits</code> bytes, so the size of a CNode in bytes is
<code class="language-plaintext highlighter-rouge">1 &lt;&lt; (CNodeSizeBits + seL4_SlotBits)</code>.</p>

<h3 id="cspaces">CSpaces</h3>

<p>A <em>CSpace</em> (capability-space) is the full range of capabilities accessible to a thread, which may be
formed of one or more CNodes. In this tutorial, we focus on the CSpace constructed for the root task
by seL4’s initialisation protocol, which consists of one CNode.</p>

<h3 id="cspace-addressing">CSpace addressing</h3>

<p>To refer to a capability and perform operations on it, you must <em>address</em> the
capability. There are two ways to address capabilities in the seL4 API. First is
by invocation, the second is by direct addressing. Invocation is a shorthand and
it is what we used to manipulate the registers of the root task’s TCB, which we
now explain in further detail.</p>

<h4 id="invocation">Invocation</h4>

<p>Each thread has a special CNode capability installed in its TCB as its <em>CSpace
root</em>. This root can be empty (a null cap), for instance when the thread is not
authorised to invoke any capabilities at all, or it can be a capability to a
CNode. The root task always has a CSpace root capability that points to a CNode.</p>

<p>In an <em>invocation</em>, a CSlot is addressed by implicitly invoking the CSpace root
of the thread that is performing the invocation. In the code example above, we
use an invocation on the <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code> CSlot to read from and write to
the registers of the TCB represented by the capability in that specific CSlot.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="n">seL4_TCB_WriteRegisters</span><span class="p">(</span><span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">num_registers</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">registers</span><span class="p">);</span>
</code></pre></div></div>

<p>This implicitly looks up the <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code> CSlot in the CNode pointed to
by the CSpace root capability of the calling thread, which here is the root task.</p>

<p>When it is clear by context and not otherwise relevant, we sometimes identify
the capability with the object it points to. So, instead of saying “the CNode
pointed to by the CSpace root capability”, we sometimes say “the CSpace root”.
If not sure, it is better to be precise. Like structs and pointers in C, objects
and capabilities are not actually interchangeable: one object can be pointed to
by multiple capabilities, and each of these capabilities could have a different
level of permissions to that object.</p>

<h4 id="direct-cspace-addressing">Direct CSpace addressing</h4>

<p>In contrast to invocation addressing, <em>direct addressing</em> allows you to specify
the CNode to look up in, rather than implicitly using the CSpace root. This form
of addressing is primarily used to construct and manipulate the shape of CSpaces
– potentially the CSpace of another thread. Note that direct addressing also
requires invocation: the operation occurs by invoking a CNode capability, which
itself is indexed from the CSpace root.</p>

<p>The following fields are used when directly addressing CSlots:</p>

<ul>
  <li><em>_service/root</em> A capability to the CNode to operate on.</li>
  <li><em>index</em> The index of the CSlot in the CNode to address.</li>
  <li><em>depth</em> How far to traverse the CNode before resolving the CSlot.</li>
</ul>

<p>For the initial, single-level CSpace, the <em>depth</em> value is always <code class="language-plaintext highlighter-rouge">seL4_WordBits</code>. For invocations, the depth is always
 implicitly <code class="language-plaintext highlighter-rouge">seL4_WordBits</code>.
More on CSpace depth will be discussed in future tutorials.</p>

<p>In the example below, we directly address the root task’s TCB to make a copy of
it in the 0th slot in the CSpace root. <a href="https://docs.sel4.systems/projects/sel4/api-doc.html#copy">CNode
copy</a> requires two
CSlots to be directly addressed: the destination CSlot, and the source CSlot.
<code class="language-plaintext highlighter-rouge">seL4_CapInitThreadCNode</code> is used in three different roles here: as source root,
as destination root, and as source slot. It is used as source and destination
root, because we are copying within the same CNode – the CNode of the initial
thread. It is used as source slot, because within the CNode of the initial
thread, <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadCNode</code> is the slot of the capability we want to copy
(and the slot <code class="language-plaintext highlighter-rouge">0</code> is the destination).</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_Error</span> <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span>
        <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span> <span class="c1">// destination root, slot, and depth</span>
        <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span> <span class="c1">// source root, slot, and depth</span>
        <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="n">seL4_NoError</span><span class="p">);</span>
</code></pre></div></div>

<p>All <a href="https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_cnode">CNode invocations</a> require direct CSpace addressing.</p>

<h3 id="initial-cspace">Initial CSpace</h3>

<p>The root task has a CSpace, set up by seL4 during boot, which contains capabilities to all
resources managed by seL4. We have already seen several capabilities in the root CSpace: <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadTCB</code>,
 and <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadCNode</code>. Both of these are specified by constants in <code class="language-plaintext highlighter-rouge">libsel4</code>, however not all initial
 capabilities are statically specified. Other capabilities are described by the <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code> data structure,
 described in <code class="language-plaintext highlighter-rouge">libsel4</code> and initialised by seL4. <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code> describes ranges of initial capabilities,
 including free slots available in the initial CSpace.</p>

<h2 id="exercises">Exercises</h2>

<p>The initial state of this tutorial provides you with the BootInfo structure,
and calculates the size (in slots) of the initial CNode object.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="kt">int</span> <span class="nf">main</span><span class="p">(</span><span class="kt">int</span> <span class="n">argc</span><span class="p">,</span> <span class="kt">char</span> <span class="o">*</span><span class="n">argv</span><span class="p">[])</span> <span class="p">{</span>

    <span class="cm">/* parse the location of the seL4_BootInfo data structure from
    the environment variables set up by the default crt0.S */</span>
    <span class="n">seL4_BootInfo</span> <span class="o">*</span><span class="n">info</span> <span class="o">=</span> <span class="n">platsupport_get_bootinfo</span><span class="p">();</span>

    <span class="kt">size_t</span> <span class="n">initial_cnode_object_size</span> <span class="o">=</span> <span class="n">BIT</span><span class="p">(</span><span class="n">info</span><span class="o">-&gt;</span><span class="n">initThreadCNodeSizeBits</span><span class="p">);</span>
    <span class="n">printf</span><span class="p">(</span><span class="s">"Initial CNode is %zu slots in size</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="n">initial_cnode_object_size</span><span class="p">);</span>
</code></pre></div></div>

<p>When you run the tutorial without changes, you will see something like the following output:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
Initial CNode is 65536 slots in size
The CNode is 0 bytes in size
&lt;&lt;seL4(CPU 0) [decodeInvocation/530 T0xffffff801ffb5400 "rootserver" @401397]: Attempted to invoke a null cap #4095.&gt;&gt;
main@main.c:33 [Cond failed: error]
    Failed to set priority
</code></pre></div></div>

<p>By the end of the tutorial all of the output will make sense. For now, the first line is from the kernel.
The second is the <code class="language-plaintext highlighter-rouge">printf</code>, telling you the size of the initial CNode.
The third line stating the number of slots in the CSpace, is incorrect, and your first task is to fix that.</p>

<h3 id="how-big-is-your-cspace">How big is your CSpace?</h3>

<p><strong>Exercise:</strong> refer to the background above, and calculate the number of bytes occupied by the initial thread’s CSpace.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="kt">size_t</span> <span class="n">initial_cnode_object_size_bytes</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span> <span class="c1">// TODO calculate this.</span>
    <span class="n">printf</span><span class="p">(</span><span class="s">"The CNode is %zu bytes in size</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="n">initial_cnode_object_size_bytes</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="kt">size_t</span> <span class="n">initial_cnode_object_size_bytes</span> <span class="o">=</span> <span class="n">initial_cnode_object_size</span> <span class="o">*</span> <span class="p">(</span><span class="mi">1u</span> <span class="o">&lt;&lt;</span> <span class="n">seL4_SlotBits</span><span class="p">);</span>
    <span class="n">printf</span><span class="p">(</span><span class="s">"The CNode is %zu bytes in size</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="n">initial_cnode_object_size_bytes</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<h3 id="copy-a-capability-between-cslots">Copy a capability between CSlots</h3>

<p>After the output showing the number of bytes in the CSpace, you will see an error:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeInvocation/530 T0xffffff801ffb5400 "rootserver" @401397]: Attempted to invoke a null cap #4095.&gt;&gt;
main@main.c:33 [Cond failed: error]
    Failed to set priority
</code></pre></div></div>

<p>The error occurs as the existing code tries to set the priority of the initial thread’s TCB by
 invoking the last CSlot in the CSpace, which is currently empty. seL4 then returns an error code,
 and our check that the operation succeeded fails.</p>

<p><strong>Exercise:</strong> fix this problem by making another copy of the TCB capability into the last slot in the CNode.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_CPtr</span> <span class="n">first_free_slot</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">start</span><span class="p">;</span>
    <span class="n">seL4_Error</span> <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                                       <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                                       <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to copy cap!"</span><span class="p">);</span>
    <span class="n">seL4_CPtr</span> <span class="n">last_slot</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">end</span> <span class="o">-</span> <span class="mi">1</span><span class="p">;</span>
    <span class="cm">/* TODO use seL4_CNode_Copy to make another copy of the initial TCB capability to the last slot in the CSpace */</span>

    <span class="cm">/* set the priority of the root task */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_SetPriority</span><span class="p">(</span><span class="n">last_slot</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="mi">10</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to set priority"</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_CPtr</span> <span class="n">first_free_slot</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">start</span><span class="p">;</span>
    <span class="n">seL4_Error</span> <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                                       <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                                       <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to copy cap!"</span><span class="p">);</span>
    <span class="n">seL4_CPtr</span> <span class="n">last_slot</span> <span class="o">=</span> <span class="n">info</span><span class="o">-&gt;</span><span class="n">empty</span><span class="p">.</span><span class="n">end</span> <span class="o">-</span> <span class="mi">1</span><span class="p">;</span>

    <span class="cm">/* use seL4_CNode_Copy to make another copy of the initial TCB capability to the last slot in the CSpace */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Copy</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                      <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span> <span class="n">seL4_AllRights</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to copy cap!"</span><span class="p">);</span>

    <span class="cm">/* set the priority of the root task */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_SetPriority</span><span class="p">(</span><span class="n">last_slot</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="mi">10</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to set priority"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On success, you will now see the output:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff801ffb5400 "rootserver" @401397]: CNode Copy/Mint/Move/Mutate: Destination not empty.&gt;&gt;
main@main.c:44 [Cond failed: error != seL4_FailedLookup]
    first_free_slot is not empty
</code></pre></div></div>

<p>Which will be fixed in the next exercise.</p>

<h3 id="how-do-you-delete-capabilities">How do you delete capabilities?</h3>

<p>The provided code checks that both <code class="language-plaintext highlighter-rouge">first_free_slot</code> and <code class="language-plaintext highlighter-rouge">last_slot</code> are empty, which of course is not
true, as you copied TCB capabilities into those CSlots. Checking if CSlots are empty is done
by a neat hack: by attempting to move the CSlots onto themselves. This should fail with an error code
<code class="language-plaintext highlighter-rouge">seL4_FailedLookup</code> if the source CSLot is empty, and an <code class="language-plaintext highlighter-rouge">seL4_DeleteFirst</code> if not.</p>

<p><strong>Exercise:</strong> delete both copies of the TCB capability.</p>

<ul>
  <li>You can either use <code class="language-plaintext highlighter-rouge">seL4_CNode_Delete</code> on the copies, or</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_CNode_Revoke</code> on the original capability to achieve this.</li>
</ul>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// TODO delete the created TCB capabilities</span>

    <span class="c1">// check first_free_slot is empty</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Move</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                            <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_FailedLookup</span><span class="p">,</span> <span class="s">"first_free_slot is not empty"</span><span class="p">);</span>

    <span class="c1">// check last_slot is empty</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Move</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                            <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_FailedLookup</span><span class="p">,</span> <span class="s">"last_slot is not empty"</span><span class="p">);</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// delete the created TCB capabilities</span>
    <span class="n">seL4_CNode_Revoke</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">seL4_CapInitThreadTCB</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>

    <span class="c1">// check first_free_slot is empty</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Move</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                            <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">first_free_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_FailedLookup</span><span class="p">,</span> <span class="s">"first_free_slot is not empty"</span><span class="p">);</span>

    <span class="c1">// check last_slot is empty</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_CNode_Move</span><span class="p">(</span><span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">,</span>
                            <span class="n">seL4_CapInitThreadCNode</span><span class="p">,</span> <span class="n">last_slot</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_FailedLookup</span><span class="p">,</span> <span class="s">"last_slot is not empty"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>On success, the output will now show:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeCNodeInvocation/106 T0xffffff801ffb5400 "rootserver" @401397]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.&gt;&gt;
&lt;&lt;seL4(CPU 0) [decodeCNodeInvocation/106 T0xffffff801ffb5400 "rootserver" @401397]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.&gt;&gt;
Suspending current thread
main@main.c:56 Failed to suspend current thread
</code></pre></div></div>

<h4 id="suspend-a-thread">Suspend a thread</h4>

<p><strong>Exercise</strong> Use <code class="language-plaintext highlighter-rouge">seL4_TCB_Suspend</code> to try and suspend the current thread.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">printf</span><span class="p">(</span><span class="s">"Suspending current thread</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
    <span class="c1">// TODO suspend the current thread</span>
    <span class="n">ZF_LOGF</span><span class="p">(</span><span class="s">"Failed to suspend current thread</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">printf</span><span class="p">(</span><span class="s">"Suspending current thread</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
    <span class="n">seL4_TCB_Suspend</span><span class="p">(</span><span class="n">seL4_CapInitThreadTCB</span><span class="p">);</span>
    <span class="n">ZF_LOGF</span><span class="p">(</span><span class="s">"Failed to suspend current thread</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On success, the output will be as follows:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeCNodeInvocation/106 T0xffffff801ffb5400 "rootserver" @401397]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.&gt;&gt;
&lt;&lt;seL4(CPU 0) [decodeCNodeInvocation/106 T0xffffff801ffb5400 "rootserver" @401397]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.&gt;&gt;
Suspending current thread
</code></pre></div></div>

<h3 id="further-exercises">Further exercises</h3>

<p>That’s all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
to become more familiar with CSpaces.</p>

<ul>
  <li>Use a data structure to track which CSlots in a CSpace are free.</li>
  <li>Make copies of the entire CSpace described by <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code></li>
  <li>Experiment with other <a href="https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_cnode">CNode invocations</a>.</li>
</ul>



<p style="text-align: right;">

      Next: <a href="/Tutorials/untyped">Untyped</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/capabilities/capabilities.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/capabilities/capabilities.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#background">Background</a>
<ul>
<li class="toc-entry toc-h3"><a href="#what-is-a-capability">What is a capability?</a></li>
<li class="toc-entry toc-h3"><a href="#cnodes-and-cslots">CNodes and CSlots</a></li>
<li class="toc-entry toc-h3"><a href="#cspaces">CSpaces</a></li>
<li class="toc-entry toc-h3"><a href="#cspace-addressing">CSpace addressing</a>
<ul>
<li class="toc-entry toc-h4"><a href="#invocation">Invocation</a></li>
<li class="toc-entry toc-h4"><a href="#direct-cspace-addressing">Direct CSpace addressing</a></li>
</ul>
</li>
<li class="toc-entry toc-h3"><a href="#initial-cspace">Initial CSpace</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#how-big-is-your-cspace">How big is your CSpace?</a></li>
<li class="toc-entry toc-h3"><a href="#copy-a-capability-between-cslots">Copy a capability between CSlots</a></li>
<li class="toc-entry toc-h3"><a href="#how-do-you-delete-capabilities">How do you delete capabilities?</a>
<ul>
<li class="toc-entry toc-h4"><a href="#suspend-a-thread">Suspend a thread</a></li>
</ul>
</li>
<li class="toc-entry toc-h3"><a href="#further-exercises">Further exercises</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/capabilities.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/capabilities.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
